Nuprl Lemma : same-sender-index 11,40
es:ES, e, e':E.
(isrcv(e))
 (isrcv(e'))
 ((e = e')
  (sender(e) = sender(e')  E & lnk(e) = lnk(e')  IdLnk & index(e) = index(e')  )) 
latex

Definitionst  T, P  Q, x:A. B(x), sender(e), lnk(e), sends(l;e), (Msg on l), ||as||, #$n, {i..j}, {x:A| B(x)} , x:AB(x), True, T, ES, E, isrcv(e), b, index(e), , s = t, Type, , IdLnk, x:A  B(x), P & Q, <a, b>, P  Q, P  Q, (e <loc e'), s ~ t, {T}, SQType(T), let x,y = A in B(x;y), t.1, False, A, i  j , left + right, P  Q, Id, loc(e), Void, a < b, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , destination(l), source(l),
Lemmases-axioms, lsrc wf, ldst wf, es-loc wf, true wf, es-loc-pred, implies functionality wrt iff, or functionality wrt iff, es-locl-iff, es-isrcv-loc, Id wf, es-locl-antireflexive, es-locl wf, IdLnk wf, es-index wf, squash wf, assert wf, es-isrcv wf, es-E wf, event system wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, es-lnk wf, es-sender wf

origin